A general translation from nested Petri nets into PROMELA

摘要

Nested Petri nets have been applied for modeling interaction protocols,mobility, adaptive systems and interorganizational workflows. However, fewresults have been reported on the use of automated tools for analyzing thebehavior of these nets. In this paper we present a general translation fromnested Petri nets into PROMELA and explain how some properties of these netscan be studied using SPIN model checker. Besides, we discuss how to deal withthe main limitations that may influence SPIN performance when verifyingpractical examples.